// Copyright 2011 Google Inc. All Rights Reserved.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

open util/ordering[State]

///////////////////////////////////////////////////////////////////////////////
// DNS is atemporal in this model

sig DomainName { }

one sig DNS {
  resolve : set (DomainName -> NetworkEndpoint)
}

///////////////////////////////////////////////////////////////////////////////
// Certificates, CAs, and HTTPS

abstract sig CertificateAuthority { }

one sig BadCA,GoodCA extends CertificateAuthority { }

sig Certificate {
	ca : CertificateAuthority,
	cn : DomainName,
	ne : NetworkEndpoint
}

///////////////////////////////////////////////////////////////////////////////

sig Path { }

abstract sig Method {}
one sig GET extends Method {}
one sig PUT  extends Method {}
one sig POST extends Method {}
one sig DELETE extends Method {}
one sig OPTIONS extends Method {}

fun safeMethods[]:set Method {
	GET+OPTIONS
}


abstract sig Status  {}
abstract sig RedirectionStatus extends Status {}
one sig c301,c302,c303,c304,c305,c306,c307 extends RedirectionStatus {}
one sig c200,c401, c404 extends Status{}

abstract sig HTTPHeader {}
abstract sig HTTPResponseHeader extends HTTPHeader{} 
abstract sig HTTPRequestHeader extends HTTPHeader{}

sig AccessControlAllowOriginHeader extends HTTPResponseHeader { 
  // We model Access-Control-Allow-Origin: * with an omitted origin field.
  origin: lone Origin 
}

sig AccessControlRequestMethodHeader extends HTTPRequestHeader {
  requestedMethod : Method
}

sig AccessControlAllowMethodsHeader extends HTTPResponseHeader {
  allowedMethods : set Method
}
{
  some allowedMethods
}

// RFC talks about having Origin Chain and not a single Origin
// We handle Origin chain by having multiple Origin Headers 
sig OriginHeader extends HTTPRequestHeader {theorigin: Origin}

sig LocationHeader extends HTTPResponseHeader {
  targetOrigin : Origin, 
  targetPath : Path
}


fact noOrphanedHeaders {
//  all h:HTTPRequestHeader|some req:HTTPRequest|h in req.headers
//  all h:HTTPResponseHeader|some resp:HTTPResponse|h in resp.headers
}

abstract sig Schema { }
one sig HTTP, HTTPS extends Schema { }

sig Origin {
  schema : Schema,
  domainName: DomainName // TODO: schema required
  
}

///////////////////////////////////////////////////////////////////////////////

abstract sig LocalState { }

one sig NoLocalState extends LocalState { }

sig PreflightRecvdState extends LocalState {
  method : Method,
  host : Origin,
  path : Path,
  headers : set HTTPRequestHeader
}

sig RedirectRecvd extends LocalState {
  method : Method,
  host : Origin,
  path : Path,
  headers : set HTTPRequestHeader
}

sig State {
  nodes : set Buffers
}

abstract sig Transition {
  fromState : one State,
  toState : one State
}
{
  toState = fromState.next
}

abstract sig RequestEvent, ResponseEvent extends Transition { }



abstract sig NetworkEndpoint { }

sig UnrestrictedNode extends NetworkEndpoint { }

sig Buffers {
  recvBuf : NetworkEndpoint -> RequestEvent,
  respBuf : RequestEvent -> ResponseEvent,
  info : NetworkEndpoint,
  localState : LocalState
}

fact Sanity_LinearTime {
  all s : State - last | one t : Transition | t.fromState = s
}

fact Sanity_NoDisassociatedBuffers {
  all buf : Buffers | some s : State | buf in s.nodes
}

///////////////////////////////////////////////////////////////////////////////

abstract sig ProcessResponse extends Transition {
  from : NetworkEndpoint,
  request : RequestEvent,
  response : ResponseEvent,
  fromLocalState : LocalState,
  toLocalState : LocalState
}
{
  some bufs : fromState.nodes, bufs' : Buffers {
    bufs.info = from
    bufs.localState = NoLocalState
    (request -> response) in bufs.respBuf
    bufs.localState = fromLocalState
    bufs'.info = from
    bufs'.localState = toLocalState
    bufs'.respBuf = bufs.respBuf - (request -> response)
    bufs'.recvBuf = bufs.recvBuf
  }
}

abstract sig HTTPRequestEvent extends RequestEvent {
  from : NetworkEndpoint,
  to : NetworkEndpoint,
  host : Origin,
  method : Method,
  path : Path,
  headers : set HTTPRequestHeader,
  cert : lone Certificate,
  fromLocalState : LocalState,
  fromLocalState' : LocalState
}
{
  some fromBufs, toBufs : fromState.nodes, toBufs' : Buffers, fromBufs' : toState.nodes {
    fromBufs.info = from
    fromBufs'.info = from
    toBufs.info = to
    toBufs'.info = to
    toBufs'.recvBuf = toBufs.recvBuf + (from -> this)
    toBufs'.respBuf = toBufs.respBuf
    toBufs'.localState = toBufs.localState
    toState.nodes = fromState.nodes - toBufs + toBufs'
    toBufs'.localState = toBufs.localState
    fromLocalState = fromBufs.localState
    fromLocalState' = fromBufs'.localState
    // toDomain, method, path, and headers are unconstrained
    to = DNS.resolve[host.domainName]
    host.schema = HTTPS implies {
      some cert
      cert.cn = host.domainName
      cert.ne = to
    }
  }
}

sig UnconstrainedHTTPRequestEvent extends HTTPRequestEvent {
}
{
  from not in Browser
  fromLocalState = NoLocalState
  fromLocalState' = NoLocalState
}

sig SameOriginRequestEvent extends HTTPRequestEvent {
}
{
  some browser : from | host = browser.pageOrigin
  fromLocalState = NoLocalState
  fromLocalState' = NoLocalState
}

sig SimpleCORSRequestEvent extends HTTPRequestEvent {
}
{
  some browser : from {
    host != browser.pageOrigin
    method in (GET + POST)
    // TOOD: more constraints required here
  }
  fromLocalState = NoLocalState
  fromLocalState' = NoLocalState
}

// Blindly pops off responses without processing them.
sig HTTPResponseEvent extends ResponseEvent {
  from : NetworkEndpoint,
  to : NetworkEndpoint,
  statusCode : Status,
  headers : set HTTPResponseHeader,
  responseTo : HTTPRequestEvent,
  cert : lone Certificate
}
{
  some fromBufs, toBufs : fromState.nodes, fromBufs', toBufs' : Buffers, toAndReq : fromBufs.recvBuf {
    from = fromBufs.info
    to = toBufs.info
    responseTo = NetworkEndpoint.toAndReq
    to = toAndReq.HTTPRequestEvent
    toBufs'.info = to
    toBufs'.respBuf = toBufs.respBuf + (responseTo->this)
    toBufs'.recvBuf = toBufs.recvBuf
    toBufs'.localState = toBufs.localState
    fromBufs'.info = to
    fromBufs'.respBuf = fromBufs.respBuf
    fromBufs'.recvBuf = fromBufs.recvBuf - toAndReq
    fromBufs'.localState = toBufs'.localState
    toState.nodes = fromState.nodes - toBufs - fromBufs + toBufs' + fromBufs'
    cert = responseTo.cert
  }
}

// Primarily to control state-space explosion. 
sig PreflightRequestEvent extends HTTPRequestEvent {
}
{
  fromLocalState = NoLocalState
  fromLocalState' = NoLocalState
  some browser : from {
    method = OPTIONS
    some AccessControlRequestMethodHeader & headers
    browser.pageOrigin != host
  }
}

sig ProcessPreflightResponse extends ProcessResponse {
}
{
  fromLocalState = NoLocalState
  from in Browser
  request in PreflightRequestEvent
  (some next : PreflightRecvdState {
     toLocalState = next
     (some allowOriginHeader : response.headers & AccessControlAllowOriginHeader |
       no allowOriginHeader.origin or allowOriginHeader.origin = from.pageOrigin)
     (some allowedMethodsHeader : response.headers & AccessControlAllowMethodsHeader |
       next.method in allowedMethodsHeader.allowedMethods)
       next.host = request.host
       next.path = request.path
     }) or toLocalState = NoLocalState
}

sig ComplexCORSRequestEvent extends HTTPRequestEvent {
}
{
  some pfState : PreflightRecvdState {
    pfState = fromLocalState
    from in Browser
    host = pfState.host
    method = pfState.method
    // TODO: where are headers?
    path = pfState.path 
    fromLocalState' = NoLocalState 
  }
}


sig ProcessRedirect extends ProcessResponse {
}
{
  from in Browser // 
  fromLocalState = NoLocalState
  response.statusCode in RedirectionStatus
  some loc : LocationHeader & response.headers, redirect : RedirectRecvd {
    redirect.host = loc.targetOrigin
    redirect.path = loc.targetPath
    redirect.headers = request.headers // TODO: model various browsers
    redirect.method = request.method // TODO: model various browsers
    toLocalState = redirect
  }
}

sig FollowRedirect extends HTTPRequestEvent {
}
{
  some redirect : RedirectRecvd {
    redirect = fromLocalState
    host = redirect.host
    method = redirect.method
    path = redirect.path
    headers = redirect.headers
    fromLocalState' = NoLocalState
  }
}

///////////////////////////////////////////////////////////////////////////////

fact InitialConditions {
  all disj buf1, buf2 : first.nodes {
    buf1.info != buf2.info
  }
  no first.nodes.recvBuf
  no first.nodes.respBuf

  first.nodes.localState = NoLocalState
}

sig Browser extends NetworkEndpoint {
  pageOrigin : Origin
}

sig StaticWebServer extends NetworkEndpoint {
  servicedPaths : set Path
}

fact StaticWebServer_RespondsTo {
  all ws:StaticWebServer, resp : HTTPResponseEvent {
    resp.from = ws implies {
      resp.responseTo.path in ws.servicedPaths implies resp.statusCode = c200
      resp.responseTo.path not in ws.servicedPaths implies resp.statusCode = c404
    }
  }
}

fact StaticWebServer_NoRequests {
  all ws:StaticWebServer, req : HTTPRequestEvent {
    req.from != ws
  }
}

sig RevokingServer extends NetworkEndpoint {
  servicedPaths : set Path
}

fact RevokingServer_RespondsUntilRevoke {
  all ws:RevokingServer, resp : HTTPResponseEvent {
    resp.from = ws implies {
      not (resp.fromState in first.next.*next)
      resp.responseTo.path in ws.servicedPaths implies resp.statusCode = c200
      resp.responseTo.path not in ws.servicedPaths implies resp.statusCode = c404
    }
  }
}

fact RevokingServer_NoRequests {
  all ws:RevokingServer, req : HTTPRequestEvent {
    req.from != ws
  }
}

///////////////////////////////////////////////////////////////////////////////

run Browser_Sanity {
} for 9 but 20 Buffers, exactly 1 Browser,
   2 StaticWebServer, 0 UnrestrictedNode, 0 RevokingServer,
   exactly 1 SameOriginRequestEvent,
   exactly 1 SimpleCORSRequestEvent,
   exactly 1 PreflightRequestEvent,
   exactly 1 ProcessRedirect,
   exactly 1 FollowRedirect,
   exactly 1 ProcessPreflightResponse,
   exactly 1 ComplexCORSRequestEvent
   

assert XD_CORS {
  all req : ComplexCORSRequestEvent {
    some browser : req.from {
      req.host != browser.pageOrigin
    }
  }
}

check XD_CORS for 7


  

pred Check_ResponseFromStaticWS {
  some resp : HTTPResponseEvent | resp.from in StaticWebServer
}


pred Check_ResponseFromRevoker {
  some resp : HTTPResponseEvent | resp.from in RevokingServer
}

assert Revoker_Revokes {
  all resp : HTTPResponseEvent {
    resp.from in RevokingServer implies resp.fromState in first.next.*next
  }
}

check Revoker_Revokes for 6 but 15 Buffers, exactly 8 State, exactly 1 RevokingServer, exactly 0 StaticWebServer, exactly 0 UnrestrictedNode, exactly 1 Browser

run Check_ResponseFromRevoker for 6 but 15 Buffers, exactly 1 RevokingServer, exactly 0 StaticWebServer, exactly 0 UnrestrictedNode, exactly 1 Browser
  

